/-
Copyright (c) 2025 Adam Topaz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Justin Curry, Adam Topaz
-/
import Mathlib.Combinatorics.Quiver.ReflQuiver
import Mathlib.Order.CompletePartialOrder
import Mathlib.Topology.Order.UpperLowerSetTopology
import Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

/-!

Let `X` be a preorder `≤`, and consider the associated Alexandrov topology on `X`.
Given a functor `F : X ⥤ C` to a complete category, we can extend `F` to a
presheaf on (the topological space) `X` by taking the right Kan extension along the canonical
functor `X ⥤ (Opens X)ᵒᵖ` sending `x : X` to the principal open `{y | x ≤ y}` in the
Alexandrov topology.

This file proves that this presheaf is a sheaf.

-/

noncomputable section

universe v u
open CategoryTheory Limits Functor
open TopCat Presheaf SheafCondition
open TopologicalSpace Topology

variable
  {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X]
  {C : Type u} [Category.{v} C] [HasLimits C]
  (F : X ⥤ C)

namespace Alexandrov

/-- Given `x : X`, this is the principal open subset of `X` generated by `x`. -/
def principalOpen (x : X) : Opens X := .mk { y | x ≤ y } <| by
  rw [IsUpperSet.isOpen_iff_isUpperSet]
  intro y z h1 h2
  exact le_trans h2 h1

lemma self_mem_principalOpen (x : X) : x ∈ principalOpen x := le_refl _

@[simp]
lemma principalOpen_le_iff {x : X} (U : Opens X) :
    principalOpen x ≤ U ↔ x ∈ U := by
  refine ⟨fun h => h <| self_mem_principalOpen _, fun hx y hy => ?_⟩
  · have := U.isOpen
    rw [IsUpperSet.isOpen_iff_isUpperSet] at this
    exact this hy hx

lemma principalOpen_le {x y : X} (h : x ≤ y) :
    principalOpen y ≤ principalOpen x :=
  fun _ hc => le_trans h hc

variable (X) in
/-- The functor sending `x : X` to the principal open associated with `x`. -/
@[simps]
def principals : X ⥤ (Opens X)ᵒᵖ where
  obj x := .op <| principalOpen x
  map {x y} f := .op <| principalOpen_le f.le |>.hom

lemma exists_le_of_le_sup {ι : Type v} {x : X}
    (Us : ι → Opens X) (h : principalOpen x ≤ iSup Us) :
    ∃ i : ι, principalOpen x ≤ Us i := by
  grind [principalOpen_le_iff, Opens.mem_iSup]

/-- The right kan extension of `F` along `X ⥤ (Opens X)ᵒᵖ`. -/
abbrev principalsKanExtension : (Opens X)ᵒᵖ ⥤ C :=
  (principals X).pointwiseRightKanExtension F

/-- Given a structured arrow `f` with domain `U : Opens X` over `principals X`,
this functor sends `f` to its "generator", an element of `X`. -/
abbrev generator (U : Opens X) :
    StructuredArrow (.op U) (principals X) ⥤ X :=
  StructuredArrow.proj (.op U) (principals X)

/-- Given a structured arrow `f` with domain `iSup Us` over `principals X`,
where `Us` is a family of `Opens X`, this functor sends `f` to the principal open
associated with it, considered as an object in the full subcategory of all `V : Opens X`
such that `V ≤ Us i` for some `i`.

This definition is primarily meant to be used in `lowerCone`, and `isLimit` below.
-/
@[simps]
def projSup {ι : Type v} (Us : ι → Opens X) :
    StructuredArrow (.op <| iSup Us) (principals X) ⥤
      (ObjectProperty.FullSubcategory fun V => ∃ i, V ≤ Us i)ᵒᵖ where
  obj f := .op <| .mk (principalOpen f.right) <| exists_le_of_le_sup Us f.hom.unop.le
  map e := .op <| LE.le.hom <| principalOpen_le <| e.right.le

variable {F} in
/-- This is an auxiliary definition which is only meant to be used in `isLimit` below. -/
@[simps]
def lowerCone
    {α : Type v} (Us : α → Opens X)
    (S : Cone ((ObjectProperty.ι fun V => ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)) :
    Cone (generator (iSup Us) ⋙ F) where
  pt := S.pt
  π := {
    app := fun f =>
      S.π.app ((projSup Us).obj f) ≫ limit.π (generator (principalOpen f.right) ⋙ F)
        ⟨.mk .unit, f.right, 𝟙 _⟩
    naturality := by
      rintro x y e
      simp only [Functor.const_obj_obj, Functor.comp_obj, Functor.const_obj_map,
        Functor.op_obj, ObjectProperty.ι_obj, Functor.pointwiseRightKanExtension_obj,
        Category.id_comp, Functor.comp_map, Category.assoc]
      rw [← S.w ((projSup Us).map e), Category.assoc]
      congr 1
      simp only [projSup_obj, Functor.comp_obj, Functor.op_obj, ObjectProperty.ι_obj,
        Functor.pointwiseRightKanExtension_obj, projSup_map, homOfLE_leOfHom, Functor.comp_map,
        Functor.op_map, Quiver.Hom.unop_op,
        Functor.pointwiseRightKanExtension_map, limit.lift_π]
      let xx : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) :=
        ⟨.mk .unit, x.right, 𝟙 _⟩
      let yy : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) :=
        ⟨.mk .unit, y.right, .op <| LE.le.hom <| principalOpen_le e.right.le⟩
      let ee : xx ⟶ yy := { left := 𝟙 _, right := e.right }
      exact limit.w
        (StructuredArrow.proj (Opposite.op (principalOpen x.right)) (principals X) ⋙ F) ee
        |>.symm
  }

/--
This is the main construction in this file showing that the right Kan extension
of `F : X ⥤ C` along `principals : X ⥤ (Opens X)ᵒᵖ` is a sheaf, by showing that a certain
cone is a limit cone.

See `isSheaf_principalsKanExtension` for the main application.
-/
def isLimit {X : TopCat.{v}} [Preorder X] [Topology.IsUpperSet X]
    (F : X ⥤ C)
    (α : Type v) (Us : α → Opens X) :
    IsLimit (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op) where
  lift S := limit.lift _ (lowerCone Us S)
  fac := by
    rintro S ⟨V, i, hV⟩
    dsimp [forget, opensLeCoverCocone]
    ext ⟨_, x, f⟩
    simp only [comp_obj, StructuredArrow.proj_obj, Category.assoc, limit.lift_π, lowerCone_pt,
      lowerCone_π_app, const_obj_obj, projSup_obj, StructuredArrow.map_obj_right, op_obj,
      ObjectProperty.ι_obj, pointwiseRightKanExtension_obj]
    have e : principalOpen x ≤ V := f.unop.le
    let VV : (ObjectProperty.FullSubcategory fun V => ∃ i, V ≤ Us i) := ⟨V, i, hV⟩
    let xx : (ObjectProperty.FullSubcategory fun V => ∃ i, V ≤ Us i) :=
      ⟨principalOpen x, i, le_trans e hV⟩
    let ee : xx ⟶ VV := e.hom
    rw [← S.w ee.op, Category.assoc]
    congr 1
    simp only [comp_obj, op_obj, ObjectProperty.ι_obj, pointwiseRightKanExtension_obj,
      Functor.comp_map, op_map, Quiver.Hom.unop_op,
      pointwiseRightKanExtension_map, limit.lift_π, xx, VV]
    congr
  uniq := by
    intro S m hm
    dsimp
    symm
    ext ⟨_, x, f⟩
    simp only [lowerCone_pt, comp_obj, limit.lift_π, lowerCone_π_app, const_obj_obj, projSup_obj,
      op_obj, ObjectProperty.ι_obj, pointwiseRightKanExtension_obj]
    specialize hm ⟨principalOpen x, ?_⟩
    · apply exists_le_of_le_sup
      exact f.unop.le
    · rw [← hm]
      simp only [mapCone_pt, Cocone.op_pt, pointwiseRightKanExtension_obj,
        const_obj_obj, comp_obj, op_obj, ObjectProperty.ι_obj, mapCone_π_app, Cocone.op_π,
        NatTrans.op_app, pointwiseRightKanExtension_map, Category.assoc, limit.lift_π]
      congr

theorem isSheaf_principalsKanExtension
    {X : TopCat.{v}} [Preorder X] [Topology.IsUpperSet X] (F : X ⥤ C) :
    Presheaf.IsSheaf (principalsKanExtension F) := by
  rw [isSheaf_iff_isSheafOpensLeCover]
  intro ι Us
  constructor
  apply isLimit

end Alexandrov

open Alexandrov

/--
The main theorem of this file.
If `X` is a topological space and preorder whose topology is the `UpperSet` topology associated
with the preorder, `F : X ⥤ C` is a functor into a complete category from the preorder category,
and `P : (Opens X)ᵒᵖ ⥤ C` denotes the right Kan extension of `F` along the
functor `X ⥤ (Open X)ᵒᵖ` which sends `x : X` to `{y | x ≤ y}`, then `P` is a sheaf.
-/
theorem Topology.IsUpperSet.isSheaf_of_isRightKanExtension
    (P : (Opens X)ᵒᵖ ⥤ C)
    (η : Alexandrov.principals X ⋙ P ⟶ F)
    [P.IsRightKanExtension η] :
    Presheaf.IsSheaf (Opens.grothendieckTopology X) P := by
  let γ : principals X ⋙ principalsKanExtension F ⟶ F :=
    (principals X).pointwiseRightKanExtensionCounit F
  let _ : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
  have : P ≅ principalsKanExtension F :=
    @rightKanExtensionUnique _ _ _ _ _ _ _ _ _ _ (by assumption) _ _ (by assumption)
  change TopCat.Presheaf.IsSheaf (X := TopCat.of X) P
  rw [isSheaf_iso_iff this]
  let _ : Preorder (TopCat.of X) := inferInstanceAs <| Preorder X
  have _ : Topology.IsUpperSet (TopCat.of X) := inferInstanceAs <| Topology.IsUpperSet X
  exact isSheaf_principalsKanExtension (X := TopCat.of X) F
